COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notions of finite union and finite sum
C00006 00003	(proof sumfacts)
C00008 00004	* bound quantifier
C00015 00005	proof of properties of union and sum
C00019 00006	a fix needed
C00027 ENDMK
C⊗;
;the notions of finite union and finite sum
(wipe-out)
(get-proofs appl prf ekl sys)
(proof sums)

(decl all (type: |ground⊗@set→truthval|) (syntype: constant))
(decl some (type: |ground⊗@set→truthval|) (syntype: constant))
(decl (numseq f) (type:|ground→ground|))
(decl sum (type: |(@numseq)⊗(@n)→(@n)|) (syntype: constant))
(decl setseq (type: |@n→@set|))
(decl un (type: |(@setseq)⊗(@n)→(@set)|) (syntype: constant))

;axiom for all
(defax all |∀n a.all(0,a)∧(all(n',a)≡a(n)∧all(n,a))|)
(label alldef)

;axiom for some
(defax some |∀n a.¬some(0,a)∧(some(n',a)≡a(n)∨some(n,a))|)
(label somedef)

;axiom for sum
(defax sum |∀n numseq.sum(numseq,0)=0∧sum(numseq,n')=sum(numseq,n)+numseq(n)|)
(label sumdef)

;axiom for un
(defax un |∀n setseq.un(setseq,0)=emptyset∧un(setseq,n')=un(setseq,n)∪setseq(n)|)
(label undef)

(decl disj_pair (type: |(@set⊗@set)→truthval|))
(define disj_pair |∀a b.disj_pair(a,b)=emptyp(a∩b)|)
(label dijpair_def)

(decl disjoint (type: |((ground→@set)⊗ground)→truthval|))
(defax disjoint |∀n setseq.disjoint(setseq,0)∧
    disjoint(setseq,n')=(disjoint(setseq,n)∧disj_pair(un(setseq,n),setseq(n)))| )
(label disjointdef)
(proof sumfacts)

;properties of all and some

(axiom |∀a n.(∀m.m<n⊃a(m))≡all(n,a)|)
(label allfact)

(axiom |∀a n.(∃m.m<n∧a(m))≡some(n,a)|)
(label somefact)

;properties of un

(axiom |∀setseq n m.m<n⊃setseq(m)⊂un(setseq,n)|)
(label unionfact1)

;exercise: unionfact2 
;∀setseq n m.n<m⊃un(setseq,n)⊂un(setseq,m)

(axiom |∀u n.n≤length u⊃(un(λm.mkset(nth(u,m)),n))=(λx.(∃k.k<n∧nth(u,k)=x))|)
(label mksetfact)

(axiom |∀u.un(λm.mkset(nth(u,m)),length u)=(λx.(mklset(u))(x))|)
(label mklset_un)

;properties of sum

(axiom |∀numseq n.(∀m.m<n⊃natnum(numseq(m)))⊃natnum(sum(numseq,n))|)
(label sumsort)

(save-proofs sums)
;* bound quantifier
    (proof allprop)

    ;we can easily prove that `all' does its job

1.  (ue ((a.|λn.all(n,a)⊃(m<n⊃a(m))|)) proof_by_induction
	 ((use transitivity_of_order) (use successor1) (open all)
	   (use less_succ_lesseq normal mode: exact) (open lesseq)))
    ;∀N.ALL(N,A)⊃(M<N⊃A(M))

2.  (ue ((a.|λn.(∀m.m<n⊃a(m))⊃all(n,a)|)) proof_by_induction (open all)
	  (use normal mode: always)
	  (use less_succ_lesseq mode: exact) (open lesseq)))
    ;∀N.(∀M.M<N⊃A(M))⊃ALL(N,A)

3.  (derive |∀n.(∀m.m<n⊃a(m))≡all(n,a)| (* -2))

    ;similarly for `some':

4.  (ue ((a.|λn.some(n,a)⊃(∃m.m<n∧a(m))|)) proof_by_induction
	 ((use transitivity_of_order) (use successor1) (open some) (part 1 (der))
	   (use less_succ_lesseq normal mode: exact) (open lesseq)))
    ;∀N.SOME(N,A)⊃(∃M.M<N∧A(M))

5.  (ue ((a.|λn.(∃m.m<n∧a(m))⊃some(n,a)|)) proof_by_induction (open some)
	  (use normal mode: always) (part 1(der))
	  (use less_succ_lesseq mode: exact) (open lesseq)))
    ;∀N.(∃M.M<N∧A(M))⊃SOME(N,A)

6.  (derive |∀n.(∃m.m<n∧a(m))≡some(n,a)| (* -2))

;proof of properties of union and sum
    (wipe-out)
    (get-proofs sums prf ekl sys)
    (proof unionprop)

    ;a property of union

    ;unionfact1

1.  (ue (a |λn.m<n⊃(∀xv.(setseq(m))(xv)⊃(un(setseq,n))(xv))|)
        proof_by_induction   
        (open un union) (use less_succ_lesseq mode: always)
        (open lesseq) (use normal mode: always))
    ;∀N.M<N⊃(∀XV.(SETSEQ(M))(XV)⊃(UN(SETSEQ,N))(XV))

    ;namely:

2.  (trw |∀setseq n m.m<n⊃setseq(m)⊂un(setseq,n)| * (open inclusion))
    (label unionfact1)

    ;a property of sum

    ;sumsort

3.  (ue (a |λn.all(n,λm.natnum numseq(m))⊃natnum sum(numseq,n)|) 
        proof_by_induction (open all sum))
    ;∀N.ALL(N,λM.NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))

4.  (rw * (use allfact mode: exact direction: reverse))
    ;∀N.(∀M.M<N⊃NATNUM(NUMSEQ(M)))⊃NATNUM(SUM(NUMSEQ,N))

    ;mksetfact

5.  (ue (a |λn.n≤length u⊃
		    (un(λm.mkset(nth(u,m)),n))(x)≡some(n,λk.x=nth(u,k))|)
	proof_by_induction 
	(part 1(open un mkset nth some union emptyset) (der))
	(use succ_lesseq_lesseq mode: always))
    ;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡SOME(N,λK.X=NTH(U,K))

6.  (rw * (use somefact 
	   ue: ((a.|λk.x=nth(u,k)|)(n.n)) mode: exact direction: reverse))
    ;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡(∃M.M<N∧X=NTH(U,M))

7.  (assume |n≤length u|)

8.  (ue ((av.|un(λm.mkset nth(u,m),n)|)
	 (bv.|λx.∃k.k<n∧nth(u,k)=x|)) set_extensionality 
	 (open epsilon)(use * -2 mode: always))
    ;UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))

9.  (ci -2)
    ;N≤LENGTH U⊃UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))

    ;mklset_un                                            

10. (ue (n |length u|) mksetfact 
	(use mklset_fact mode: exact direction: reverse) (open lesseq))
    ;∀U.UN(λM.MKSET(NTH(U,M)),LENGTH U)=MKLSET(U)

    ;;;;;;;
    ;used here:

    ;labels: TRANS_LESSEQ 
    ;∀N M K.N≤M∧M≤K⊃N≤K

    ;labels: SET_EXTENSIONALITY 
    ;∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV

    ;labels: SOMEFACT 
    ;∀A N.(∃M.M<N∧A(M))≡SOME(N,A)

    ;labels: MKLSET_FACT 
    ;∀U.MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))
    ;namely:
;a fix needed
;fixed

(define consnumber |consnumber(0)=nil∧consnumber(n')=n.consnumber(n)|
        inductive_definition)

(trw |∀n.natnum consnumber(n)|)
;∀N.NATNUM(CONSNUMBER(N))

(axiom |∀numseq n.all(n,λm.natnum(numseq(m)))⊃natnum(sum(numseq,n))|)